The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(2^n, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(S(x'), S(x)) → h(g(x', S(x)), f(S(S(S(x'))), x))
g(S(x), S(x')) → h(f(S(x), S(x')), g(x, S(S(S(x')))))
h(0, S(x)) → h(0, x)
h(0, 0) → 0
g(S(x), 0) → 0
f(S(x), 0) → 0
h(S(x), x2) → h(x, x2)
g(0, x2) → 0
f(0, x2) → 0

Rewrite Strategy: INNERMOST

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

f(S(x'), S(x)) → h(g(x', S(x)), f(S(S(S(x'))), x))
g(S(x), S(x')) → h(f(S(x), S(x')), g(x, S(S(S(x')))))
h(0, S(x)) → h(0, x)
h(0, 0) → 0
g(S(x), 0) → 0
f(S(x), 0) → 0
h(S(x), x2) → h(x, x2)
g(0, x2) → 0
f(0, x2) → 0

S is empty.
Rewrite Strategy: INNERMOST

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(2ⁿ):
The rewrite sequence
f(S(S(x14_1)), S(x)) →⁺ h(h(h(g(x14_1, S(x)), f(S(S(S(x14_1))), x)), g(x14_1, S(S(S(x))))), f(S(S(S(S(x14_1)))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,1].
The pumping substitution is [x / S(x)].
The result substitution is [x14_1 / S(x14_1)].

The rewrite sequence
f(S(S(x14_1)), S(x)) →⁺ h(h(h(g(x14_1, S(x)), f(S(S(S(x14_1))), x)), g(x14_1, S(S(S(x))))), f(S(S(S(S(x14_1)))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x / S(x)].
The result substitution is [x14_1 / S(S(x14_1))].

(4) BOUNDS(2^n, INF)